A:Type, eq:EqDecider(A), B:(AType), f, g, h:a:A fp B(a). f || g  h  f || h  g 

latex

Definitions	f(a), x(s), f(x), <a, b>, s = t, left + right, P  Q, x:AB(x), P  Q, x:A. B(x), x. t(x), x:A  B(x), P & Q, P  Q, , b, A, t  T, Unit, f  g, f || g, a:A fp B(a), Type, EqDecider(T), if b then t else f fi , False
Lemmas	fpf-join-ap-sq, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, fpf-join-dom